module SMap = Map.Make(String);;
module SSet = Set.Make(String);;

type term = Const of string
	    | Var of string
	    | FuncApp of string*(term list);;
type pre = PPredicate of string*(term list)
	   | NPredicate of string*(term list)
	   | PConjunction of pre*pre
	   | Disjunction of pre*pre
	   | Exists of string*pre
	   | Equal of term*term
	   | NEqual of term*term;;
type cl = CPredicate of string*(term list)
	  | Truth
	  | CConjunction of cl*cl
	  | Leadsto of pre*cl
	  | Forall of string*cl;;

let freevar_from_term ?(bound = SSet.empty) term =
  match term with
    | Var(x) ->
	if (SSet.mem x bound) then
	  SSet.empty
	else
	  SSet.add x SSet.empty
    | _ -> SSet.empty;;

let freevars_in_termlist ?(bound = SSet.empty) termlist =
  List.fold_left (fun varset term ->
		    let freevar = (freevar_from_term ~bound:bound term) in
		      SSet.union freevar varset
		 ) SSet.empty termlist;;

let rec freevars_in_pre ?(bound = SSet.empty) pre =
  match pre with
    | (PPredicate(_, termlist) | NPredicate(_, termlist)) ->
	freevars_in_termlist ~bound:bound termlist
    | (PConjunction(pre1, pre2) | Disjunction(pre1, pre2)) ->
	SSet.union (freevars_in_pre ~bound:bound pre1) (freevars_in_pre ~bound:bound pre2)
    | Exists(x, pre) ->
	freevars_in_pre ~bound:(SSet.add x bound) pre
    | (Equal(term1, term2) | NEqual(term1, term2)) ->
	SSet.union
	  (freevar_from_term ~bound:bound term1)
	  (freevar_from_term ~bound:bound term2);;

let rec string_of_term term =
  match term with
    | Const(c) -> c
    | Var(x) -> x
    | FuncApp(func, termlist) ->
	string_of_predicate func termlist
and string_of_predicate rel termlist =
  let (term, trest) = ((List.hd termlist), (List.tl termlist)) in
    rel ^ "(" ^ (string_of_term term) ^
      (List.fold_left (
	 fun termstring term ->
	   termstring ^ ", " ^ (string_of_term term)) "" trest)
    ^ ")";;

let rec string_of_pre pred =
  match pred with
    | PPredicate(rel, termlist) ->
	string_of_predicate rel termlist
    | NPredicate(rel, termlist) ->
	"!" ^ (string_of_predicate rel termlist)
    | PConjunction(pre1, pre2) ->
	Printf.sprintf "%s & %s" (string_of_pre pre1) (string_of_pre pre2)
    | Disjunction(pre1, pre2) ->
	Printf.sprintf "%s | %s" (string_of_pre pre1) (string_of_pre pre2)
    | Exists(str, pre) ->
	Printf.sprintf "(E %s.%s)" str (string_of_pre pre)
    | Equal(term1, term2) ->
	Printf.sprintf "%s = %s" (string_of_term term1) (string_of_term term2)
    | NEqual(term1, term2) ->
	Printf.sprintf "%s != %s" (string_of_term term1) (string_of_term term2);;

let rec string_of_cl clause =
  match clause with
    | CPredicate(rel, termlist) ->
	string_of_predicate rel termlist
    | Truth -> "1"
    | CConjunction(cl1, cl2) ->
	Printf.sprintf "%s & %s" (string_of_cl cl1) (string_of_cl cl2)
    | Leadsto(pre, cl) ->
	Printf.sprintf "(%s => %s)" (string_of_pre pre) (string_of_cl cl)
    | Forall(str, cl) ->
	Printf.sprintf "(A %s.%s)" str (string_of_cl cl);;
